(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (str.suffixof (str.substr var2 var4 var4) (str.replace "8jh{R{M#W_" var0 var2)))
(assert (str.contains var1 var1))
(assert (str.suffixof var0 "*""}AX-9,_f"))
(assert (str.contains (str.replace var1 var2 var0) (str.replace (str.substr "p+k\\\\B|r3v" 2 var3) (str.replace var0 var1 "XGh8Ms1Y)F") (str.at var2 var3))))
(check-sat)
